(g,n,e,z. n  e)  g:IMonoid|(<+>hgrp)||g|(True)|g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, Mon, AbMon, Group{i}, AbGrp, OCMon, OGrp
Definitions	t  T, , x:A. B(x), T, IMonoid
Lemmas	imon wf, int add grp wf2, hgrp of ocgrp wf, grp car wf, true wf, squash wf, mon nat op wf2